(0) Obligation:
Clauses:
div(X, s(Y), Z) :- div_s(X, Y, Z).
div_s(0, Y, 0).
div_s(s(X), Y, 0) :- lss(X, Y).
div_s(s(X), Y, s(Z)) :- ','(sub(X, Y, R), div_s(R, Y, Z)).
lss(s(X), s(Y)) :- lss(X, Y).
lss(0, s(Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
Query: div(g,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
lssA(s(X1), s(X2)) :- lssA(X1, X2).
div_sB(s(X1), X2, 0) :- lssA(X1, X2).
div_sB(s(X1), X2, s(X3)) :- subC(X1, X2, X4).
div_sB(s(X1), X2, s(X3)) :- ','(subcC(X1, X2, X4), div_sB(X4, X2, X3)).
subC(s(X1), s(X2), X3) :- subC(X1, X2, X3).
divD(X1, s(X2), X3) :- div_sB(X1, X2, X3).
Clauses:
lsscA(s(X1), s(X2)) :- lsscA(X1, X2).
lsscA(0, s(X1)).
div_scB(0, X1, 0).
div_scB(s(X1), X2, 0) :- lsscA(X1, X2).
div_scB(s(X1), X2, s(X3)) :- ','(subcC(X1, X2, X4), div_scB(X4, X2, X3)).
subcC(s(X1), s(X2), X3) :- subcC(X1, X2, X3).
subcC(X1, 0, X1).
Afs:
divD(x1, x2, x3) = divD(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divD_in: (b,b,f)
div_sB_in: (b,b,f)
lssA_in: (b,b)
subC_in: (b,b,f)
subcC_in: (b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
DIVD_IN_GGA(X1, s(X2), X3) → U7_GGA(X1, X2, X3, div_sB_in_gga(X1, X2, X3))
DIVD_IN_GGA(X1, s(X2), X3) → DIV_SB_IN_GGA(X1, X2, X3)
DIV_SB_IN_GGA(s(X1), X2, 0) → U2_GGA(X1, X2, lssA_in_gg(X1, X2))
DIV_SB_IN_GGA(s(X1), X2, 0) → LSSA_IN_GG(X1, X2)
LSSA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, lssA_in_gg(X1, X2))
LSSA_IN_GG(s(X1), s(X2)) → LSSA_IN_GG(X1, X2)
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → U3_GGA(X1, X2, X3, subC_in_gga(X1, X2, X4))
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → SUBC_IN_GGA(X1, X2, X4)
SUBC_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, subC_in_gga(X1, X2, X3))
SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → U4_GGA(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U4_GGA(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → U5_GGA(X1, X2, X3, div_sB_in_gga(X4, X2, X3))
U4_GGA(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → DIV_SB_IN_GGA(X4, X2, X3)
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2), X3) → U13_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
div_sB_in_gga(
x1,
x2,
x3) =
div_sB_in_gga(
x1,
x2)
lssA_in_gg(
x1,
x2) =
lssA_in_gg(
x1,
x2)
subC_in_gga(
x1,
x2,
x3) =
subC_in_gga(
x1,
x2)
subcC_in_gga(
x1,
x2,
x3) =
subcC_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
0 =
0
subcC_out_gga(
x1,
x2,
x3) =
subcC_out_gga(
x1,
x2,
x3)
DIVD_IN_GGA(
x1,
x2,
x3) =
DIVD_IN_GGA(
x1,
x2)
U7_GGA(
x1,
x2,
x3,
x4) =
U7_GGA(
x1,
x2,
x4)
DIV_SB_IN_GGA(
x1,
x2,
x3) =
DIV_SB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x2,
x3)
LSSA_IN_GG(
x1,
x2) =
LSSA_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x1,
x2,
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
SUBC_IN_GGA(
x1,
x2,
x3) =
SUBC_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIVD_IN_GGA(X1, s(X2), X3) → U7_GGA(X1, X2, X3, div_sB_in_gga(X1, X2, X3))
DIVD_IN_GGA(X1, s(X2), X3) → DIV_SB_IN_GGA(X1, X2, X3)
DIV_SB_IN_GGA(s(X1), X2, 0) → U2_GGA(X1, X2, lssA_in_gg(X1, X2))
DIV_SB_IN_GGA(s(X1), X2, 0) → LSSA_IN_GG(X1, X2)
LSSA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, lssA_in_gg(X1, X2))
LSSA_IN_GG(s(X1), s(X2)) → LSSA_IN_GG(X1, X2)
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → U3_GGA(X1, X2, X3, subC_in_gga(X1, X2, X4))
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → SUBC_IN_GGA(X1, X2, X4)
SUBC_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, subC_in_gga(X1, X2, X3))
SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → U4_GGA(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U4_GGA(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → U5_GGA(X1, X2, X3, div_sB_in_gga(X4, X2, X3))
U4_GGA(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → DIV_SB_IN_GGA(X4, X2, X3)
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2), X3) → U13_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
div_sB_in_gga(
x1,
x2,
x3) =
div_sB_in_gga(
x1,
x2)
lssA_in_gg(
x1,
x2) =
lssA_in_gg(
x1,
x2)
subC_in_gga(
x1,
x2,
x3) =
subC_in_gga(
x1,
x2)
subcC_in_gga(
x1,
x2,
x3) =
subcC_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
0 =
0
subcC_out_gga(
x1,
x2,
x3) =
subcC_out_gga(
x1,
x2,
x3)
DIVD_IN_GGA(
x1,
x2,
x3) =
DIVD_IN_GGA(
x1,
x2)
U7_GGA(
x1,
x2,
x3,
x4) =
U7_GGA(
x1,
x2,
x4)
DIV_SB_IN_GGA(
x1,
x2,
x3) =
DIV_SB_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x2,
x3)
LSSA_IN_GG(
x1,
x2) =
LSSA_IN_GG(
x1,
x2)
U1_GG(
x1,
x2,
x3) =
U1_GG(
x1,
x2,
x3)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
SUBC_IN_GGA(
x1,
x2,
x3) =
SUBC_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 9 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2), X3) → U13_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
subcC_in_gga(
x1,
x2,
x3) =
subcC_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
0 =
0
subcC_out_gga(
x1,
x2,
x3) =
subcC_out_gga(
x1,
x2,
x3)
SUBC_IN_GGA(
x1,
x2,
x3) =
SUBC_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUBC_IN_GGA(s(X1), s(X2), X3) → SUBC_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
SUBC_IN_GGA(
x1,
x2,
x3) =
SUBC_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUBC_IN_GGA(s(X1), s(X2)) → SUBC_IN_GGA(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SUBC_IN_GGA(s(X1), s(X2)) → SUBC_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LSSA_IN_GG(s(X1), s(X2)) → LSSA_IN_GG(X1, X2)
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2), X3) → U13_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
subcC_in_gga(
x1,
x2,
x3) =
subcC_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
0 =
0
subcC_out_gga(
x1,
x2,
x3) =
subcC_out_gga(
x1,
x2,
x3)
LSSA_IN_GG(
x1,
x2) =
LSSA_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LSSA_IN_GG(s(X1), s(X2)) → LSSA_IN_GG(X1, X2)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LSSA_IN_GG(s(X1), s(X2)) → LSSA_IN_GG(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- LSSA_IN_GG(s(X1), s(X2)) → LSSA_IN_GG(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(20) YES
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIV_SB_IN_GGA(s(X1), X2, s(X3)) → U4_GGA(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U4_GGA(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → DIV_SB_IN_GGA(X4, X2, X3)
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2), X3) → U13_gga(X1, X2, X3, subcC_in_gga(X1, X2, X3))
subcC_in_gga(X1, 0, X1) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, X3, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
subcC_in_gga(
x1,
x2,
x3) =
subcC_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
0 =
0
subcC_out_gga(
x1,
x2,
x3) =
subcC_out_gga(
x1,
x2,
x3)
DIV_SB_IN_GGA(
x1,
x2,
x3) =
DIV_SB_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(22) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV_SB_IN_GGA(s(X1), X2) → U4_GGA(X1, X2, subcC_in_gga(X1, X2))
U4_GGA(X1, X2, subcC_out_gga(X1, X2, X4)) → DIV_SB_IN_GGA(X4, X2)
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2)) → U13_gga(X1, X2, subcC_in_gga(X1, X2))
subcC_in_gga(X1, 0) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The set Q consists of the following terms:
subcC_in_gga(x0, x1)
U13_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(24) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
DIV_SB_IN_GGA(s(X1), X2) → U4_GGA(X1, X2, subcC_in_gga(X1, X2))
U4_GGA(X1, X2, subcC_out_gga(X1, X2, X4)) → DIV_SB_IN_GGA(X4, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( U4_GGA(x1, ..., x3) ) = 2x2 + 2x3 + 2
POL( subcC_in_gga(x1, x2) ) = 2x1
POL( s(x1) ) = 2x1 + 2
POL( U13_gga(x1, ..., x3) ) = 2x3
POL( 0 ) = 2
POL( subcC_out_gga(x1, ..., x3) ) = 2x3
POL( DIV_SB_IN_GGA(x1, x2) ) = 2x1 + 2x2 + 1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
subcC_in_gga(s(X1), s(X2)) → U13_gga(X1, X2, subcC_in_gga(X1, X2))
subcC_in_gga(X1, 0) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
(25) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
subcC_in_gga(s(X1), s(X2)) → U13_gga(X1, X2, subcC_in_gga(X1, X2))
subcC_in_gga(X1, 0) → subcC_out_gga(X1, 0, X1)
U13_gga(X1, X2, subcC_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), s(X2), X3)
The set Q consists of the following terms:
subcC_in_gga(x0, x1)
U13_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(26) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(27) YES